Lambda the Ultimate

Automated Whitebox Fuzz Testing. Patrice Godefroid; Michael Levin; David Molnar.

Fuzz testing is an effective technique for finding security vulnerabilities in software. Traditionally, fuzz testing tools apply random mutations to well-formed inputs and test the program on the resulting values. We present an alternative whitebox fuzz testing approach inspired by recent advances in symbolic execution and dynamic test generation. Our approach records an actual run of a program under test on a well-formed input, symbolically evaluates the recorded trace, and generates constraints capturing how the program uses its inputs. The generated constraints are used to produce new inputs which cause the program to follow different control paths. This process is repeated with the help of a code-coverage maximizing heuristic designed to find defects as fast as possible. We have implemented this algorithm in SAGE (Scalable, Automated, Guided Execution), a new tool employing x86 instruction-level tracing and emulation for whitebox fuzzing of arbitrary file-reading Windows applications.

I wonder how moving this type of system to the level of high-level programming language would impact its effectiveness.

Chung-chieh Shan and I have submitted a paper on delimited contexts in operating systems and the zipper OS (which has not been formally published). Systems programmers do use contexts whether they are aware of that or not. The first version of UNIX on PDP-7 already implemented delimited continuations, in the form of co-routines between user programs and the shell. Being aware of delimited continuations may help systems programmers to better implement context switching, signal handling, etc., using the techniques developed in programming language research. It also leads to new insights, for example, that checkpointing a process and snapshotting a file system are essentially the same activity.

The final paper is available at http://okmij.org/ftp/papers/context-OS.pdf

There is little new there for long-time LtU members; however, this time the material is presented systematically and in context.

Type-sensitive control-flow analysis, John Reppy, 2006 ML Workshop.

Higher-order typed languages, such as ML, provide strong support for data and type abstraction. While such abstraction is often viewed as costing performance, there are situations where it may provide opportunities for more aggressive program optimization. Specifically, we can exploit the fact that type abstraction guarantees representation independence, which allows the compiler to specialize data representations. This paper describes a first step in supporting such optimizations; namely a modular control-flow analysis that uses the program’s type information to compute more precise results. We present our algorithm as an extension of Serrano’s version of 0-CFA and we show that it respects types. We also discuss applications of the analysis with a specific focus on optimizing Concurrent ML programs.

Andrej Bauer has made available his tutorial slides on Synthetic Computability, which he gave at the Mathematical Foundations of Programming Semantics #23 conference last month.

He motivates the idea of a synthetic theory, with reference to Hyland's construction of Eff (the effective topos), and tackles the ideas lying behind synthetic domain theory, one of the most rarefied areas of PL semantics, as accessibly as I have seen it done.

Highly theoretical, highly recommended. Via Bauer's announcement at his Mathematics and Computation weblog.

The Festschrift for John C Reynolds's 70th Birthday is available as Special Issue of Theoretical Computer Science, Vol 375(1-3), 1 May 2007. Many interesting papers! Get it while it's hot.

Don Stewart, John Goerzen and I are excited to announce that we're working on a book for O'Reilly, the title of which is "Real-World Haskell". We hope that the book will be useful for getting people quickly bootstrapped into applying Haskell to real problems, and shedding the language's undeserved "academic only" aura. We're delighted that O'Reilly has agreed to publish the book under a Creative Commons license, so we'll be able to make it available to as many people as possible.

For more information, see our web site.

Following on from last year, I've started organising an AngloHaskell event for 2007. It's early days yet, but planning is taking place on the haskell wiki at http://www.haskell.org/haskellwiki/AngloHaskell and on #anglohaskell on irc.freenode.net - anyone who might attend is welcome to join in the discussion.

Last year's event was good fun, featuring practically-oriented and hobbyist talks, punting and plenty of pub time. The organisation process may seem a little haphazard, but an important part of laziness is being able to evaluate things when they are in fact demanded! On that basis, a time and a venue are the first order of business.

It is argued that formal verifications of programs, no matter how obtained, will not play the same key role in the development of computer science and software engineering as proofs do in mathematics. Furthermore, the absence of continuity, the inevitability of change, and the complexity of specification of significantly many real progarms make the formal verification process difficult to justify and manage. It is felt that ease of formal verification should not dominate program language deisgn.

Jed Donnelley, Alan Karp, and I would like your comments on our draft paper

Delegating Responsibility in Digital Systems:
Horton's "Who Done It?"

Programs do good things, but also do bad,
making software security more than a fad.
The authority of programs, we do need to tame.
But bad things still happen. Who do we blame?

From the very beginnings of access control:
Should we be safe by construction,
or should we patrol?
Horton shows how, in an elegant way,
we can simply do both, and so save the day.

with apologies to Dr. Seuss

We plan to submit it to USENIX HotSec 07 (Hot Topics in Security) which has a five page limit. Submission deadline is 6/1/2007. We think this paper is important. Your comments and suggestions will be greatly appreciated. Thanks!

Local Reasoning for Storable Locks and Threads. Alexey Gotsman; Josh Berdine; Byron Cook; Noam Rinetzky; Mooly Sagiv.

We present a resource-oriented program logic that is able to reason about concurrent heap-manipulating programs with unbounded numbers of dynamically-allocated locks and threads. The logic is inspired by concurrent separation logic, but handles these more realistic concurrency primitives. We demonstrate that the proposed logic allows for local reasoning about programs that exhibit a high degree of information hiding in their locking mechanisms. Soundness is proved using a novel thread-local fixed-point semantics.